YES 2.365
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
  ↳ LR
mainModule List
|  | ((group :: [Ordering]  ->  [[Ordering]]) :: [Ordering]  ->  [[Ordering]]) | 
module List where
|  | import qualified Maybe import qualified Prelude
 
 
 | 
|  | group :: Eq a => [a]  ->  [[a]] 
 
 | 
|  | groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]] 
 
| groupBy | _ [] | = | [] |  
| groupBy | eq (x : xs) | = | 
| (x : ys) : groupBy eq zs | where |  |  |  
 | 
module Maybe where
|  | import qualified List import qualified Prelude
 
 
 | 
Lambda Reductions:
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
mainModule List
|  | ((group :: [Ordering]  ->  [[Ordering]]) :: [Ordering]  ->  [[Ordering]]) | 
module List where
|  | import qualified Maybe import qualified Prelude
 
 
 | 
|  | group :: Eq a => [a]  ->  [[a]] 
 
 | 
|  | groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]] 
 
| groupBy | _ [] | = | [] |  
| groupBy | eq (x : xs) | = | 
| (x : ys) : groupBy eq zs | where |  |  |  
 | 
module Maybe where
|  | import qualified List import qualified Prelude
 
 
 | 
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(wu : wv)
is replaced by the following term
wu : wv
↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
mainModule List
|  | ((group :: [Ordering]  ->  [[Ordering]]) :: [Ordering]  ->  [[Ordering]]) | 
module List where
|  | import qualified Maybe import qualified Prelude
 
 
 | 
|  | group :: Eq a => [a]  ->  [[a]] 
 
 | 
|  | groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]] 
 
| groupBy | vw [] | = | [] |  
| groupBy | eq (x : xs) | = | 
| (x : ys) : groupBy eq zs | where |  |  |  
 | 
module Maybe where
|  | import qualified List import qualified Prelude
 
 
 | 
Cond Reductions:
The following Function with conditions
is transformed to
| undefined0 | True | = undefined | 
| undefined1 |  | = undefined0 False | 
The following Function with conditions
| span | p [] | = ([],[]) | 
| span | p (wu : wv) |  | 
is transformed to
| span | p [] | = span3 p [] | 
| span | p (wu : wv) | = span2 p (wu : wv) | 
| span2 | p (wu : wv) | = 
| span1 p wu wv (p wu) | | where | 
| span0 | p wu wv True | = ([],wu : wv) |  |  |  | 
| span1 | p wu wv True | = (wu : ys,zs) |  | span1 | p wu wv False | = span0 p wu wv otherwise |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  | 
| span3 | p [] | = ([],[]) | 
| span3 | xv xw | = span2 xv xw | 
↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
mainModule List
|  | ((group :: [Ordering]  ->  [[Ordering]]) :: [Ordering]  ->  [[Ordering]]) | 
module List where
|  | import qualified Maybe import qualified Prelude
 
 
 | 
|  | group :: Eq a => [a]  ->  [[a]] 
 
 | 
|  | groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]] 
 
| groupBy | vw [] | = | [] |  
| groupBy | eq (x : xs) | = | 
| (x : ys) : groupBy eq zs | where |  |  |  
 | 
module Maybe where
|  | import qualified List import qualified Prelude
 
 
 | 
Let/Where Reductions:
The bindings of the following Let/Where expression
| (x : ys) : groupBy eq zs | | where |  | 
|  |  | 
|  |  | 
|  |  | 
|  |  | 
are unpacked to the following functions on top level
| groupByYs0 | xx xy xz (ys,vx) | = ys | 
| groupByVv10 | xx xy xz | = span (xx xy) xz | 
| groupByZs0 | xx xy xz (vy,zs) | = zs | 
| groupByYs | xx xy xz | = groupByYs0 xx xy xz (groupByVv10 xx xy xz) | 
| groupByZs | xx xy xz | = groupByZs0 xx xy xz (groupByVv10 xx xy xz) | 
The bindings of the following Let/Where expression
| span1 p wu wv (p wu) | | where | 
| span0 | p wu wv True | = ([],wu : wv) |  | 
|  | 
| span1 | p wu wv True | = (wu : ys,zs) |  | span1 | p wu wv False | = span0 p wu wv otherwise |  | 
|  |  | 
|  |  | 
|  |  | 
|  |  | 
|  |  | 
are unpacked to the following functions on top level
| span2Zs | yu yv | = span2Zs1 yu yv (span2Vu43 yu yv) | 
| span2Ys1 | yu yv (ys,wx) | = ys | 
| span2Vu43 | yu yv | = span yu yv | 
| span2Zs1 | yu yv (ww,zs) | = zs | 
| span2Span1 | yu yv p wu wv True | = (wu : span2Ys yu yv,span2Zs yu yv) | 
| span2Span1 | yu yv p wu wv False | = span2Span0 yu yv p wu wv otherwise | 
| span2Span0 | yu yv p wu wv True | = ([],wu : wv) | 
| span2Ys | yu yv | = span2Ys1 yu yv (span2Vu43 yu yv) | 
↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
mainModule List
|  | (group :: [Ordering]  ->  [[Ordering]]) | 
module List where
|  | import qualified Maybe import qualified Prelude
 
 
 | 
|  | group :: Eq a => [a]  ->  [[a]] 
 
 | 
|  | groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]] 
 
| groupBy | vw [] | = | [] |  
| groupBy | eq (x : xs) | = | (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs) |  
 | 
|  | 
| groupByVv10 | xx xy xz | = | span (xx xy) xz |  
 | 
|  | 
| groupByYs | xx xy xz | = | groupByYs0 xx xy xz (groupByVv10 xx xy xz) |  
 | 
|  | 
| groupByYs0 | xx xy xz (ys,vx) | = | ys |  
 | 
|  | 
| groupByZs | xx xy xz | = | groupByZs0 xx xy xz (groupByVv10 xx xy xz) |  
 | 
|  | 
| groupByZs0 | xx xy xz (vy,zs) | = | zs |  
 | 
module Maybe where
|  | import qualified List import qualified Prelude
 
 
 | 
Haskell To QDPs
↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs(:(GT, yw3111)) → new_span2Zs(yw3111)
new_span2Ys(:(GT, yw3111)) → new_span2Zs(yw3111)
new_span2Ys(:(GT, yw3111)) → new_span2Ys(yw3111)
new_span2Zs(:(GT, yw3111)) → new_span2Ys(yw3111)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Ys(:(GT, yw3111)) → new_span2Ys(yw3111)
 The graph contains the following edges 1 > 1
- new_span2Ys(:(GT, yw3111)) → new_span2Zs(yw3111)
 The graph contains the following edges 1 > 1
- new_span2Zs(:(GT, yw3111)) → new_span2Ys(yw3111)
 The graph contains the following edges 1 > 1
- new_span2Zs(:(GT, yw3111)) → new_span2Zs(yw3111)
 The graph contains the following edges 1 > 1
↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs0(:(EQ, yw3111)) → new_span2Ys0(yw3111)
new_span2Ys0(:(EQ, yw3111)) → new_span2Zs0(yw3111)
new_span2Ys0(:(EQ, yw3111)) → new_span2Ys0(yw3111)
new_span2Zs0(:(EQ, yw3111)) → new_span2Zs0(yw3111)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Ys0(:(EQ, yw3111)) → new_span2Zs0(yw3111)
 The graph contains the following edges 1 > 1
- new_span2Ys0(:(EQ, yw3111)) → new_span2Ys0(yw3111)
 The graph contains the following edges 1 > 1
- new_span2Zs0(:(EQ, yw3111)) → new_span2Zs0(yw3111)
 The graph contains the following edges 1 > 1
- new_span2Zs0(:(EQ, yw3111)) → new_span2Ys0(yw3111)
 The graph contains the following edges 1 > 1
↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs1(:(LT, yw3111)) → new_span2Zs1(yw3111)
new_span2Ys1(:(LT, yw3111)) → new_span2Zs1(yw3111)
new_span2Zs1(:(LT, yw3111)) → new_span2Ys1(yw3111)
new_span2Ys1(:(LT, yw3111)) → new_span2Ys1(yw3111)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs1(:(LT, yw3111)) → new_span2Zs1(yw3111)
 The graph contains the following edges 1 > 1
- new_span2Zs1(:(LT, yw3111)) → new_span2Ys1(yw3111)
 The graph contains the following edges 1 > 1
- new_span2Ys1(:(LT, yw3111)) → new_span2Zs1(yw3111)
 The graph contains the following edges 1 > 1
- new_span2Ys1(:(LT, yw3111)) → new_span2Ys1(yw3111)
 The graph contains the following edges 1 > 1
↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_groupBy(:(yw30, yw31)) → new_groupBy(new_groupByZs0(yw30, yw31))
The TRS R consists of the following rules:
new_span2Zs2(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Zs4([]) → []
new_groupByZs0(GT, :(GT, yw311)) → new_span2Zs2(yw311)
new_groupByZs0(LT, :(GT, yw311)) → :(GT, yw311)
new_span2Zs3(:(EQ, yw3111)) → new_span2Zs12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Ys3([]) → []
new_span2Ys3(:(GT, yw3111)) → []
new_span2Ys12(yw3111, yw7, yw6) → :(EQ, yw7)
new_span2Ys3(:(EQ, yw3111)) → new_span2Ys12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Zs12(yw3111, yw13, yw12) → yw12
new_groupByZs0(GT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Zs3(:(GT, yw3111)) → :(GT, yw3111)
new_groupByZs0(yw30, []) → []
new_groupByZs0(EQ, :(LT, yw311)) → :(LT, yw311)
new_span2Ys4(:(EQ, yw3111)) → []
new_groupByZs0(EQ, :(EQ, yw311)) → new_span2Zs3(yw311)
new_span2Zs4(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Ys2(:(EQ, yw3111)) → []
new_span2Zs4(:(LT, yw3111)) → new_span2Zs10(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_groupByZs0(LT, :(LT, yw311)) → new_span2Zs4(yw311)
new_groupByZs0(LT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Ys2([]) → []
new_span2Zs4(:(GT, yw3111)) → :(GT, yw3111)
new_span2Ys2(:(GT, yw3111)) → new_span2Ys10(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Zs11(yw3111, yw15, yw14) → yw14
new_span2Zs3([]) → []
new_groupByZs0(EQ, :(GT, yw311)) → :(GT, yw311)
new_span2Zs2([]) → []
new_span2Ys3(:(LT, yw3111)) → []
new_span2Ys4(:(LT, yw3111)) → new_span2Ys11(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_span2Ys11(yw3111, yw5, yw4) → :(LT, yw5)
new_span2Zs2(:(LT, yw3111)) → :(LT, yw3111)
new_span2Ys4([]) → []
new_span2Zs3(:(LT, yw3111)) → :(LT, yw3111)
new_groupByZs0(GT, :(LT, yw311)) → :(LT, yw311)
new_span2Ys10(yw3111, yw9, yw8) → :(GT, yw9)
new_span2Zs2(:(GT, yw3111)) → new_span2Zs11(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Ys2(:(LT, yw3111)) → []
new_span2Zs10(yw3111, yw11, yw10) → yw10
new_span2Ys4(:(GT, yw3111)) → []
The set Q consists of the following terms:
new_span2Ys2([])
new_span2Zs12(x0, x1, x2)
new_groupByZs0(GT, :(EQ, x0))
new_groupByZs0(EQ, :(LT, x0))
new_span2Zs11(x0, x1, x2)
new_groupByZs0(EQ, :(EQ, x0))
new_span2Ys10(x0, x1, x2)
new_span2Ys3(:(EQ, x0))
new_span2Ys4(:(EQ, x0))
new_groupByZs0(GT, :(LT, x0))
new_span2Ys3([])
new_span2Ys2(:(EQ, x0))
new_groupByZs0(LT, :(LT, x0))
new_span2Ys3(:(LT, x0))
new_span2Zs4(:(GT, x0))
new_span2Ys2(:(GT, x0))
new_span2Ys4([])
new_span2Zs4(:(LT, x0))
new_span2Ys12(x0, x1, x2)
new_groupByZs0(GT, :(GT, x0))
new_span2Zs3(:(GT, x0))
new_groupByZs0(LT, :(GT, x0))
new_span2Zs10(x0, x1, x2)
new_span2Zs3(:(LT, x0))
new_span2Zs3([])
new_span2Zs2(:(EQ, x0))
new_span2Ys4(:(LT, x0))
new_groupByZs0(x0, [])
new_span2Ys4(:(GT, x0))
new_span2Ys3(:(GT, x0))
new_span2Zs3(:(EQ, x0))
new_span2Zs4([])
new_span2Zs2(:(GT, x0))
new_span2Ys2(:(LT, x0))
new_span2Zs2([])
new_groupByZs0(LT, :(EQ, x0))
new_span2Zs2(:(LT, x0))
new_span2Ys11(x0, x1, x2)
new_groupByZs0(EQ, :(GT, x0))
new_span2Zs4(:(EQ, x0))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_groupBy(:(yw30, yw31)) → new_groupBy(new_groupByZs0(yw30, yw31))
The remaining pairs can at least be oriented weakly.
none
Used ordering:  Polynomial interpretation [25]:
POL(:(x1, x2)) = 1 + x2   
POL(EQ) = 0   
POL(GT) = 0   
POL(LT) = 0   
POL([]) = 0   
POL(new_groupBy(x1)) = x1   
POL(new_groupByZs0(x1, x2)) = x2   
POL(new_span2Ys10(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys11(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys12(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys2(x1)) = 1 + x1   
POL(new_span2Ys3(x1)) = x1   
POL(new_span2Ys4(x1)) = x1   
POL(new_span2Zs10(x1, x2, x3)) = x3   
POL(new_span2Zs11(x1, x2, x3)) = x3   
POL(new_span2Zs12(x1, x2, x3)) = 1 + x3   
POL(new_span2Zs2(x1)) = x1   
POL(new_span2Zs3(x1)) = x1   
POL(new_span2Zs4(x1)) = x1   
The following usable rules [17] were oriented:
new_span2Zs2(:(LT, yw3111)) → :(LT, yw3111)
new_span2Ys4(:(EQ, yw3111)) → []
new_groupByZs0(GT, :(LT, yw311)) → :(LT, yw311)
new_span2Ys2(:(GT, yw3111)) → new_span2Ys10(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Ys3(:(GT, yw3111)) → []
new_span2Ys4([]) → []
new_span2Zs3(:(GT, yw3111)) → :(GT, yw3111)
new_span2Zs4(:(GT, yw3111)) → :(GT, yw3111)
new_span2Zs2(:(GT, yw3111)) → new_span2Zs11(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Zs3(:(EQ, yw3111)) → new_span2Zs12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Ys3(:(LT, yw3111)) → []
new_span2Zs3(:(LT, yw3111)) → :(LT, yw3111)
new_groupByZs0(yw30, []) → []
new_span2Zs3([]) → []
new_groupByZs0(LT, :(LT, yw311)) → new_span2Zs4(yw311)
new_groupByZs0(LT, :(GT, yw311)) → :(GT, yw311)
new_span2Ys11(yw3111, yw5, yw4) → :(LT, yw5)
new_groupByZs0(EQ, :(LT, yw311)) → :(LT, yw311)
new_span2Ys4(:(GT, yw3111)) → []
new_span2Zs4(:(LT, yw3111)) → new_span2Zs10(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_groupByZs0(EQ, :(GT, yw311)) → :(GT, yw311)
new_groupByZs0(GT, :(GT, yw311)) → new_span2Zs2(yw311)
new_groupByZs0(GT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Zs10(yw3111, yw11, yw10) → yw10
new_span2Ys3([]) → []
new_span2Zs2([]) → []
new_span2Zs2(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Ys2(:(LT, yw3111)) → []
new_groupByZs0(EQ, :(EQ, yw311)) → new_span2Zs3(yw311)
new_groupByZs0(LT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Zs4(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Ys2([]) → []
new_span2Zs4([]) → []
new_span2Zs12(yw3111, yw13, yw12) → yw12
new_span2Ys3(:(EQ, yw3111)) → new_span2Ys12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Ys4(:(LT, yw3111)) → new_span2Ys11(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_span2Ys10(yw3111, yw9, yw8) → :(GT, yw9)
new_span2Zs11(yw3111, yw15, yw14) → yw14
new_span2Ys2(:(EQ, yw3111)) → []
new_span2Ys12(yw3111, yw7, yw6) → :(EQ, yw7)
↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ PisEmptyProof
Q DP problem:
P is empty.
The TRS R consists of the following rules:
new_span2Zs2(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Zs4([]) → []
new_groupByZs0(GT, :(GT, yw311)) → new_span2Zs2(yw311)
new_groupByZs0(LT, :(GT, yw311)) → :(GT, yw311)
new_span2Zs3(:(EQ, yw3111)) → new_span2Zs12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Ys3([]) → []
new_span2Ys3(:(GT, yw3111)) → []
new_span2Ys12(yw3111, yw7, yw6) → :(EQ, yw7)
new_span2Ys3(:(EQ, yw3111)) → new_span2Ys12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Zs12(yw3111, yw13, yw12) → yw12
new_groupByZs0(GT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Zs3(:(GT, yw3111)) → :(GT, yw3111)
new_groupByZs0(yw30, []) → []
new_groupByZs0(EQ, :(LT, yw311)) → :(LT, yw311)
new_span2Ys4(:(EQ, yw3111)) → []
new_groupByZs0(EQ, :(EQ, yw311)) → new_span2Zs3(yw311)
new_span2Zs4(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Ys2(:(EQ, yw3111)) → []
new_span2Zs4(:(LT, yw3111)) → new_span2Zs10(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_groupByZs0(LT, :(LT, yw311)) → new_span2Zs4(yw311)
new_groupByZs0(LT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Ys2([]) → []
new_span2Zs4(:(GT, yw3111)) → :(GT, yw3111)
new_span2Ys2(:(GT, yw3111)) → new_span2Ys10(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Zs11(yw3111, yw15, yw14) → yw14
new_span2Zs3([]) → []
new_groupByZs0(EQ, :(GT, yw311)) → :(GT, yw311)
new_span2Zs2([]) → []
new_span2Ys3(:(LT, yw3111)) → []
new_span2Ys4(:(LT, yw3111)) → new_span2Ys11(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_span2Ys11(yw3111, yw5, yw4) → :(LT, yw5)
new_span2Zs2(:(LT, yw3111)) → :(LT, yw3111)
new_span2Ys4([]) → []
new_span2Zs3(:(LT, yw3111)) → :(LT, yw3111)
new_groupByZs0(GT, :(LT, yw311)) → :(LT, yw311)
new_span2Ys10(yw3111, yw9, yw8) → :(GT, yw9)
new_span2Zs2(:(GT, yw3111)) → new_span2Zs11(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Ys2(:(LT, yw3111)) → []
new_span2Zs10(yw3111, yw11, yw10) → yw10
new_span2Ys4(:(GT, yw3111)) → []
The set Q consists of the following terms:
new_span2Ys2([])
new_span2Zs12(x0, x1, x2)
new_groupByZs0(GT, :(EQ, x0))
new_groupByZs0(EQ, :(LT, x0))
new_span2Zs11(x0, x1, x2)
new_groupByZs0(EQ, :(EQ, x0))
new_span2Ys10(x0, x1, x2)
new_span2Ys3(:(EQ, x0))
new_span2Ys4(:(EQ, x0))
new_groupByZs0(GT, :(LT, x0))
new_span2Ys3([])
new_span2Ys2(:(EQ, x0))
new_groupByZs0(LT, :(LT, x0))
new_span2Ys3(:(LT, x0))
new_span2Zs4(:(GT, x0))
new_span2Ys2(:(GT, x0))
new_span2Ys4([])
new_span2Zs4(:(LT, x0))
new_span2Ys12(x0, x1, x2)
new_groupByZs0(GT, :(GT, x0))
new_span2Zs3(:(GT, x0))
new_groupByZs0(LT, :(GT, x0))
new_span2Zs10(x0, x1, x2)
new_span2Zs3(:(LT, x0))
new_span2Zs3([])
new_span2Zs2(:(EQ, x0))
new_span2Ys4(:(LT, x0))
new_groupByZs0(x0, [])
new_span2Ys4(:(GT, x0))
new_span2Ys3(:(GT, x0))
new_span2Zs3(:(EQ, x0))
new_span2Zs4([])
new_span2Zs2(:(GT, x0))
new_span2Ys2(:(LT, x0))
new_span2Zs2([])
new_groupByZs0(LT, :(EQ, x0))
new_span2Zs2(:(LT, x0))
new_span2Ys11(x0, x1, x2)
new_groupByZs0(EQ, :(GT, x0))
new_span2Zs4(:(EQ, x0))
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.